package esctest;

public class Bag {

	/**
	 * What the bag is holding.
	 */
	/*@
	  @ invariant a != null;
	  @*/
	int[] a;

	/**
	 * Number of things in the bag.
	 */
	/*@
	  @ invariant n >= 0 && n <= a.length;
	  @*/
	int n;

	/*@
	  @ public normal_behavior
	  @ requires input != null;
	  @ ensures n == \old(input.length);
	  @ ensures a.length == \old(input.length);
	  @*/
	public Bag(int[] input) {
		n = input.length;
		a = new int[n];
		System.arraycopy(input, 0, a, 0, n);
	}

	/*@
	  @ requires n >= 1;
	  @*/
	public int extractMin() {
		int m = Integer.MAX_VALUE;
		int mindex = 0;
		for (int i = 0; i < n; i++) {
			if (a[i] < m) {
				mindex = i;
				m = a[i];
			}
		}
		n--;
		a[mindex] = a[n];
		return m;
	}
	
	 
	 /*@
	   @ normal_behavior
	   @ requires (\exists int i; i >= 0 && i < n; a[i]%2 == 1);
	   @ ensures \result%2 == 1;
	   @ ensures n == \old(n)-1;
	   @ also
	   @ normal_behavior
	   @ requires (\forall int i; i>=0 && i < n; a[i]%2 == 0);
	   @ ensures \result == 0;
	   @ ensures n == \old(n);
	   @*/
	 public int extractFirstOdd(){
		 int m = 0;
		 int mindex = 0;
		 boolean oddfound = false;
		 
		 for(int i = 0; i<n; i++){
			 if(a[i]%2 == 1){
				 mindex = i;
				 m = a[i];
				 oddfound = true;
				 break;
			 }
		 }
		 
		 if(oddfound){
			 n--;
			 a[mindex]=a[n];
		 }
		 
		 
		 return m;
	 }
	
	
	
}
